Inference at * 2 2 1 2 
Iof proof for Lemma p-fun-exp-add-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
9. (n = 0)
10. (n+m = 0)
11. (n = 0)
12. (m = 0)
  (f o f^n  (do-apply(f^m - 1;x))) ~ (f o f^n - 1  (do-apply(f o f^m - 1  ;x))) 

latex

 by (RW (AddrC [2;2] (UnfoldsC ``p-compose``)) 0) 
CollapseTHEN ((RepUR ``do-apply`` ( 0)) 

CoCollapseTHEN ((Fold `do-apply` 0) 
CollapseTHEN (((if (0
C) =0 then SplitOnConclITE else SplitOnHypITE (0))) 
CollapseTHENA (Auto)))) 

latex

C1: .....truecase..... NILNIL

C1: 13. can-apply(f^m - 1;x)
C1:   (f o f^n  (do-apply(f^m - 1;x))) ~ (f o f^n - 1  (outl(f(do-apply(f^m - 1;x)))))
C2: .....falsecase..... NILNIL

C2: 13. (can-apply(f^m - 1;x))
C2:   (f o f^n  (do-apply(f^m - 1;x))) ~ (f o f^n - 1  (outl(f^m - 1(x))))
C.

Definitions	f o g  , do-apply(f;x), left + right, Unit, t  T, P  Q, P & Q, x:A  B(x), A, b, s = t, , x:A. B(x), P  Q, x:AB(x)
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot